/*
Copyright 2008 Nicola Olivetti, Gian Luca Pozzato

    This file is part of GoalDuck.

    GoalDuck is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    GoalDuck is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with GoalDuck.  If not, see <http://www.gnu.org/licenses/>.
*/

/* leanCK */
:- op(400,fy,neg), 
   op(500,xfy,and), 
   op(600,xfy,or),
   op(650,xfy,->), 
   op(650,xfy,=>).
:-use_module(library(lists)).


/* --------------------------------------------------------------------------------------- */

/* The following predicate implements the calculi:

   		prove(Fml,UnExp,Lits,Trans,Labels)

  Fml is the formula currently being expanded
  UnExp is the list of formulas on the branch not yet considered
  Lits is the list of literals (i.e. x: P, x: neg P, with P \in ATM) occurring in the current branch
  Trans is the list of transitions (i.e. x-A->y, neg (x-A->y)) occurring in the current branch
  Labels is the list of labels in the current branch

  Labelled formulas are represented as follows:
  - world formulas x: A  --->  [x,a]
  - transition formulas 
      x-A->y  --->  [x,a,y]
		neg (x-A->y)  --->  [neg,x,a,y]

  prove(F,[],[],[]) succeeds if and only if the formula neg F is valid in conditional logic CK 
  
*/

/* Classification of Smullyan */

type([X,A and B],conjunction,[X,A],[X,B]).
type([X,neg (A or B)],conjunction,[X,neg A],[X,neg B]).
type([X,neg (A -> B)],conjunction,[X,A],[X,neg B]).
type([X,neg (A and B)],disjunction,[X,neg A],[X,neg B]).
type([X,A or B],disjunction,[X,A],[X,B]).
type([X,A -> B],disjunction,[X,neg A],[X,B]).


prove(neg neg A,UnExp,Lits,Trans,Labels,Cond):-!,
  prove(A,UnExp,Lits,Trans,Labels,Cond).

prove(Fml,UnExp,Lits,Trans,Labels,Cond):-
  type(Fml,conjunction,Alpha1,Alpha2),!,
  prove(Alpha1,[Alpha2|UnExp],Lits,Trans,Labels,Cond).

prove(Fml,UnExp,Lits,Trans,Labels,Cond):-
  type(Fml,disjunction,Beta1,Beta2),!,
  prove(Beta1,UnExp,Lits,Trans,Labels,Cond),
  prove(Beta2,UnExp,Lits,Trans,Labels,Cond).

prove([X,neg (A => B)],UnExp,Lits,Trans,Labels,Cond):-!,
  generaLabels(Y,Labels),
  prove([X,A,Y],[[Y,neg B]|UnExp],Lits,Trans,[Y|Labels],Cond).


prove([X,A => B],UnExp,Lits,Trans,Labels,Cond):-
  select([[X,A => B],Used],Cond,NewCond),!,
  member(Y,Labels),
  \+member(Y,Used),
  append(UnExp,[[X,A => B]],NewUnExp),
  prove([Y,B],NewUnExp,Lits,Trans,Labels,[[[X,A => B],[Y|Used]]|NewCond]),
  prove([neg,X,A,Y],NewUnExp,Lits,Trans,Labels,[[[X,A => B],[Y|Used]]|NewCond]).
prove([X,A => B],UnExp,Lits,Trans,Labels,Cond):-!,
  member(Y,Labels),
  append(UnExp,[[X,A => B]],NewUnExp),
  prove([Y,B],NewUnExp,Lits,Trans,Labels,[[[X,A => B],[Y]]|Cond]),
  prove([neg,X,A,Y],NewUnExp,Lits,Trans,Labels,[[[X,A => B],[Y]]|Cond]).
  

prove([X,L1],_,[[X,L2]|Lits],_,_,_):-
  (L1=L2,!) ; prove([X,L1],[],Lits,[],[],[]).
prove([X,neg L],[Next|UnExp],Lits,Trans,Labels,Cond):-!,
  prove(Next,UnExp,[[X,L]|Lits],Trans,Labels,Cond).
prove([X,L],[Next|UnExp],Lits,Trans,Labels,Cond):-!,
  prove(Next,UnExp,[[X,neg L]|Lits],Trans,Labels,Cond).

prove([X,A,Y],_,_,[[U,B,V]|Trans],_,_):-
  (X=U,Y=V,prove([x,A],[[x,neg B]],[],[],[x],[]),prove([x,neg A],[[x,B]],[],[],[x],[]),!) ;
  prove([X,A,Y],[],[],Trans,[],[]).
prove([neg,X,A,Y],_,_,[[neg,U,B,V]|Trans],_,_):-
  (X=U,Y=V,prove([x,A],[[x,neg B]],[],[],[x],[]),prove([x,neg A],[[x,B]],[],[],[x],[]),!) ;
  prove([neg,X,A,Y],[],[],Trans,[],[]).
prove([neg,X,A,Y],[Next|UnExp],Lits,Trans,Labels,Cond):-!,
  prove(Next,UnExp,Lits,[[X,A,Y]|Trans],Labels,Cond).
prove([X,A,Y],[Next|UnExp],Lits,Trans,Labels,Cond):-!,
  prove(Next,UnExp,Lits,[[neg,X,A,Y]|Trans],Labels,Cond).



thm(Fml):-prove([x,neg (Fml)],[],[],[],[x],[]).




/* --------------------------------------------------------------------------------------- */


/* This predicate generates a "new" label for that branch */
generaLabels(x,Labels):-true,\+member(x,Labels),!.
generaLabels(y,Labels):-true,\+member(y,Labels),!.
generaLabels(z,Labels):-true,\+member(z,Labels),!.
generaLabels(u,Labels):-true,\+member(z,Labels),!.
generaLabels(v,Labels):-true,\+member(z,Labels),!.
generaLabels(w,Labels):-true,\+member(z,Labels),!.
generaLabels(k,Labels):-true,\+member(k,Labels),!.
generaLabels(j,Labels):-true,\+member(j,Labels),!.
generaLabels(i,Labels):-true,\+member(i,Labels),!.
generaLabels(x+1,[i|_]):-!.
generaLabels(x+N1,[Last|_]):-Last=x+N,N1 is N+1,!.